CoinductiveBuiltinNatural.agda:11,21-22
ℕ !=< ∞ ℕ
when checking that the expression suc has type ℕ → ℕ
